$\forall$$T$:Type, $L$:$T$ List, $P_{1}$, $P_{2}$, $Q_{1}$, $Q_{2}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop), $R_{1}$, $R_{2}$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop).
\\[0ex]($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $P_{1}$($i$) $\Rightarrow$ $P_{2}$($i$))
\\[0ex]$\Rightarrow$ ($\forall$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $Q_{2}$($i$) $\Rightarrow$ $Q_{1}$($i$))
\\[0ex]$\Rightarrow$ ($\forall$$i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $R_{1}$($i$,$j$) $\Rightarrow$ $R_{2}$($i$,$j$))
\\[0ex]$\Rightarrow$ causal\_order($L$;$R_{1}$;$P_{1}$;$Q_{1}$)
\\[0ex]$\Rightarrow$ causal\_order($L$;$R_{2}$;$P_{2}$;$Q_{2}$)